$\forall$${\it es}$:ES, ${\it Fail}$:AbsInterface(Top), $A$:Type, $X$:AbsInterface($A$). alive($X$) $\in$ AbsInterface($A$)